package tableaux.blocking;

import java.util.Set;

import kb.RBox;
import kb.TBox;

import entities.Individual;
import entities.concept.Concept;
import entities.concept.UniversalConcept;
import entities.role.Role;

public class OptimizedDoubleBlocking implements Blocking {

	/**
	 * Note: for logic ALCIO Given any individual n, check if any other
	 * individual that has an order < that of n blocks n. Consequence:
	 * generating rules (e.g., exists rule) will be blocked for this n. Note:
	 * non-generating rules are still applicable to this node n.
	 * 
	 * <br>
	 * 
	 * Instead of implementing double blocking (cf. Horrocks SHOIQ procedure),
	 * an optimized blocking is implemented: see ECAI 2002 Horrocks, Sattler
	 * paper.
	 * 
	 * @return
	 */
	public boolean canBeBlocked(Individual w, TBox tb) {
		// indirectly blocked if any of its non-nominal predecessor is blocked
		Individual pred = w.getGeneratingParents();
		if (pred != null && (pred.isBlockable() || pred.isBlocked())) {
			w.setBlockStatus(true);
			return true;
		}
		// directly blocked?
		Set<Individual> ancs = w.getGeneratingAncestors(false);
		ancs.remove(w);
		Individual.ancChecked.clear();
		// System.err.println("Ancs for "+this+": "+ancs.size());
		for (Individual anc : ancs) {
			if (anc.isBlockable() && anc.isBlocked()) {
				// condition 1: none of its blockable ancestors are blocked
				return false;
			}
		}
		for (Individual wprime : ancs) {
			// condition 2: subset label of any ancestor
			if (!wprime.getLabels().containsAll(w.getLabels())) {
				continue;
			}
			// if this ancestor has any forall restriction, check for condition
			// 3:  all inv-R parent carry C for restriction All R.C, i.e., no
			// further expansion needed
			boolean pass = true;
			for (Concept c : wprime.getLabels()) {
				if (c instanceof UniversalConcept) {
					Role s = ((UniversalConcept) c).getRole();
					Concept filler = ((UniversalConcept) c).getFiller();
					pass &= checkInvRoleFiller(w, pred, s, filler, tb);
					if (!pass) {
						return false;
					}
				}
			}
			if (pass) {
				w.setBlockStatus(true);
//				System.out.println("blocked: "+w);
				return true;
			}
		}
		return false;
	}

	/*
	 * For a given All S.C, find  inv-S  of ``this"
	 * individual, check if the parents have C in the labels.
	 */
	private boolean checkInvRoleFiller(Individual w, Individual v, Role s, Concept c, TBox tb) {
		Role is = tb.getRoleBox().getInverseRole(s);
		Set<Individual> parents = w.getParents(is, tb);
		if (parents == null || parents.size() < 1 || !parents.contains(v)) {
			return true;
		}
		RBox rb = tb.getRoleBox();
		boolean more = rb.isComplexRole(s);
		//the inv-S predecessor must have C
		if (!v.getLabels().contains(c)) {
			return false;
		}
		//its predecessor must have all R.C for all transitive subroles R
		if(more){
			for(Role r:rb.getAllSubRoles(s)){
				if(rb.isTransitive(r)){
					// this parent is a inv-R successor of ind, then it must have All R.C in it.
					Role ir = rb.getInverseRole(r);
					Set<Individual> rps = w.getParents(ir, tb);
					if(rps.contains(v)){
						UniversalConcept transuc = new UniversalConcept(r,c);
						if (!v.getLabels().contains(transuc)) {
							return false;
						}
					}
				}
			}
		}

		return true;
//		Role is = tb.getRoleBox().getInverseRole(s);
//		Set<Individual> parents = w.getParents(is, tb);
//		if (parents == null || parents.size() < 1) {
//			return true;
//		}
//		RBox rb = tb.getRoleBox();
//		boolean more = rb.isComplexRole(s);
//		//the inv-S predecessor must have C
//		for (Individual n : parents) {
//			if(!ancs.contains(n)){
//				continue;
//			}
//			if (!n.getLabels().contains(c)) {
//				return false;
//			}
//			//its predecessor must have all R.C for all transitive subroles R
//			if(more){
//				for(Role r:rb.getAllSubRoles(s)){
//					if(rb.isTransitive(r)){
//						// this parent is a inv-R successor of ind, then it must have All R.C in it.
//						Role ir = rb.getInverseRole(r);
//						Set<Individual> rps = w.getParents(ir, tb);
//						if(rps.contains(n)){
//							UniversalConcept transuc = new UniversalConcept(r,c);
//							if (!n.getLabels().contains(transuc)) {
//								return false;
//							}
//						}
//					}
//				}
//			}
//		}
//
//		return true;
	}

}
